*****ASSUME ∃n.(¬(n=zero)∧¬integer pred1(n,zero));

1 ∃n.(¬(n=zero)∧¬integer pred1(n,zero))  (1)

*****∃E ↑ n;

2 ¬(n=zero)∧¬integer pred1(n,zero)  (2)

*****∧I induction;

3 (¬integer pred1(n,zero)∧∀n1.(¬integer pred1(n,n1)⊃¬integer pred1(n,succ n1)))⊃∀n1.¬integer pred1(n,n1)  

*****∀E pred2 n,n1;

4 pred1(n,n1)=IF succ n1=n THEN n1 ELSE pred1(n,succ n1)  

*****DISTRIB;

5 pred1(n,n1)=IF succ n1=n THEN n1 ELSE pred1(n,succ n1)≡IF succ n1=n THEN pred1(n,n1)=n1 ELSE pred1(n,n1)=pred1%
(n,succ n1)  

*****TAUT succ n1=n⊃pred1(n,n1)=n1 ↑↑:↑;

6 succ n1=n⊃pred1(n,n1)=n1  

*****TAUT ¬(succ n1=n)⊃pred1(n,n1)=pred1(n,succ n1) ↑↑↑:↑↑;

7 ¬(succ n1=n)⊃pred1(n,n1)=pred1(n,succ n1)  

*****ASSUME ¬integer pred1(n,n1);

8 ¬integer pred1(n,n1)  (8)

*****∀E integer n1;

9 integer n1  

*****TAUTEQ ¬integer pred1(n,succ n1) 6:↑;

10 ¬integer pred1(n,succ n1)  (8)

*****⊃I ↑↑↑⊃↑;

11 ¬integer pred1(n,n1)⊃¬integer pred1(n,succ n1)  

*****∀I ↑ n1;

12 ∀n1.(¬integer pred1(n,n1)⊃¬integer pred1(n,succ n1))  

*****TAUT ∀n1.¬integer pred1(n,n1) 2:3,↑;

13 ∀n1.¬integer pred1(n,n1)  (2)

*****∧I induction;

14 ((¬(zero=zero)⊃∃m.succ m=zero)∧∀n.((¬(n=zero)⊃∃m.succ m=n)⊃(¬(succ n=zero)⊃∃m.succ m=succ n)))⊃∀n.(¬(n=zero)⊃%
∃m.succ m=n)  

*****TAUTEQ succ n=succ n ;

15 succ n=succ n  

*****∃I ↑ n←m OCC ((1));

16 ∃m.succ m=succ n  

*****TAUT (¬(n=zero)⊃∃m.succ m=n)⊃(¬(succ n=zero)⊃∃m.succ m=succ n) ↑;

17 (¬(n=zero)⊃∃m.succ m=n)⊃(¬(succ n=zero)⊃∃m.succ m=succ n)  

*****∀I ↑ n;

18 ∀n.((¬(n=zero)⊃∃m.succ m=n)⊃(¬(succ n=zero)⊃∃m.succ m=succ n))  

*****TAUTEQ ∀n.(¬(n=zero)⊃∃m.succ m=n) 14,↑;

19 ∀n.(¬(n=zero)⊃∃m.succ m=n)  

*****∀E pred2 succ m,m;

20 pred1(succ m,m)=IF succ m=succ m THEN m ELSE pred1(succ m,succ m)  

*****DISTRIB;

21 pred1(succ m,m)=IF succ m=succ m THEN m ELSE pred1(succ m,succ m)≡IF succ m=succ m THEN pred1(succ m,m)=m ELS%
E pred1(succ m,m)=pred1(succ m,succ m)  

*****TAUT succ m=succ m⊃pred1(succ m,m)=m ↑↑:↑;

22 succ m=succ m⊃pred1(succ m,m)=m  

*****TAUTEQ pred1(succ m,m)=m ↑;

23 pred1(succ m,m)=m  

*****∀E integer m;

24 integer m  

*****TAUTEQ integer pred1(succ m,m) ↑↑:↑;

25 integer pred1(succ m,m)  

*****∀I ↑ m;

26 ∀m.integer pred1(succ m,m)  

*****∀E 19 n;

27 ¬(n=zero)⊃∃m.succ m=n  

*****TAUT ∃m.succ m=n 2,↑;

28 ∃m.succ m=n  (2)

*****∃E ↑ m;

29 succ m=n  (29)

*****SUBST ↑ IN 13;

30 ∀n1.¬integer pred1(succ m,n1)  (2 29)

*****∀E ↑ m;

31 ¬integer pred1(succ m,m)  (2 29)

*****TAUT FALSE 25,↑;

32 FALSE  (1)

*****⊃I 1⊃↑;

33 ∃n.(¬(n=zero)∧¬integer pred1(n,zero))⊃FALSE  

*****TAUT ¬∃n.(¬(n=zero)∧¬integer pred1(n,zero)) ↑;

34 ¬∃n.(¬(n=zero)∧¬integer pred1(n,zero))  

*****PUSH ↑;

35 ∀n.¬(¬(n=zero)∧¬integer pred1(n,zero))  

*****∀E ↑ n;

36 ¬(¬(n=zero)∧¬integer pred1(n,zero))  

*****∀E pred1 n;

37 pred n=pred1(n,zero)  

*****TAUTEQ ¬(n=zero)⊃integer pred n ↑↑:↑;

38 ¬(n=zero)⊃integer pred n  

*****∀I ↑ n;

39 ∀n.(¬(n=zero)⊃integer pred n)